package tr.edu.ege.kipler.satisfiability.completion.rules.formula;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.completion.rules.CompletionRule;
import tr.edu.ege.kipler.satisfiability.container.WcsData;
import tr.edu.ege.kipler.syntax.BinaryBooleanExpression;
import tr.edu.ege.kipler.syntax.WorldElement;
import tr.edu.ege.kipler.syntax.BinaryBooleanExpression.Operator;
import tr.edu.ege.kipler.syntax.atomicformula.Formula;

/**
 * This rule finds all the conjunctions in the current world and adds both
 * operands of a conjunction to the current world.
 * 
 * @author İnanç Seylan
 * 
 */
public class ConjunctionRule extends CompletionRule {
	private boolean applied;

	public boolean isApplied() {
		return applied;
	}

	/**
	 * For all formulae in this world, call
	 * {@link #decomposeConjunction(Formula)}.
	 * 
	 * @see tr.edu.ege.seagent.alcbi.satisfiability.frame.CompletionRule#apply()
	 */
	public void apply() throws UnsatisfiableException {
		applied = false;
		for (WorldElement f : getWorld().getPBox().getFormulas()) {
			decomposeConjunction(f);
		}
	}

	/**
	 * Any one operand or both operands of a conjunction can also be a
	 * conjunction. This method allows to handle multiple levels of conjunctive
	 * formulae by recursively calling itself on the operands of the
	 * (conjunctive) formula given.
	 * 
	 * @param f
	 *            The formula to be decomposed if it's a conjunction of course
	 */
	private void decomposeConjunction(WorldElement f)
			throws UnsatisfiableException {
		if (f instanceof BinaryBooleanExpression) {
			BinaryBooleanExpression bf = (BinaryBooleanExpression) f;
			if (bf.getOperator().equals(Operator.AND)) {
				WcsData wcsData = getWcs().getData();
				if (!getWorld().contains(bf.getLhs())) {
					wcsData.getLogger().info(
							"WCS " + getWcs().getId()
									+ " Conjunction rule: Adding "
									+ bf.getLhs());
					wcsData.getDependencyManager().move(bf.getLhs(), bf);
					getWorld().add(bf.getLhs());
					decomposeConjunction(bf.getLhs());
					applied = true;
				}
				if (!getWorld().contains(bf.getRhs())) {
					wcsData.getLogger().info(
							"WCS " + getWcs().getId()
									+ " Conjunction rule: Adding "
									+ bf.getRhs());
					wcsData.getDependencyManager().move(bf.getRhs(), bf);
					getWorld().add(bf.getRhs());
					decomposeConjunction(bf.getRhs());
					applied = true;
				}
			}
		}
	}
}
